import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertSame;
import static org.junit.Assert.assertTrue;

import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.io.File;
import java.io.IOException;

import javax.swing.Timer;

import model.BasicParameter;
import model.cnf.CNF;
import model.cnf.FileCNF;
import model.solver.IllegalSolverArgumentException;
import model.solver.RSatParameter;
import model.solver.SolverParameter;
import model.solver.SolverResult;
import model.solver.SolverResultStatus;

import org.junit.Before;
import org.junit.Test;

import controller.solver.RSat;

public class TestRSat {

	private File	solverDirectory;
	private RSat	sat;

	@Before
	public void setUp() {
		try
		{
			solverDirectory = new File("solveur");

			sat = new RSat(solverDirectory);
		} catch (IOException e)
		{
			e.printStackTrace();
			return;
		}
	}

	@Test
	public void testRSat() {
		assertTrue("rsat use timeout", sat.hasTimeout());
	}

	@Test
	public void testGetCommandLine() {
		String cnfFile = "./tstcnf/unsat.cnf";
		RSatParameter param = sat.getRSatParameter();

		String[] tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong source", tab[1], cnfFile);

		// change timout
		param.setTimeOut(4000);

		tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong source", tab[1], cnfFile);
		assertEquals("wrong parameter : wrong arg for timeout", tab[2], "-t");
		assertEquals("wrong parameter : wrong timeout", tab[3], String.valueOf(param.getTimeOut() / 1000));

		// change print solution
		param.setPrintSolution(true);
		tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong source", tab[1], cnfFile);
		assertEquals("wrong parameter : wrong arg for timeout", tab[2], "-t");
		assertEquals("wrong parameter : wrong timeout", tab[3], String.valueOf(param.getTimeOut() / 1000));
		assertEquals("wrong parameter : wrong arg for print option", tab[4], "-s");

		// verifie applique pas de delay
		param.setTimeOut(BasicParameter.NO_DELAY);
		tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong source", tab[1], cnfFile);
		assertEquals("wrong parameter : wrong arg for print option", tab[2], "-s");
	}

	@Test
	public void testDetectUnsat() {
		String cnfFile = "./tstcnf/unsat.cnf";
		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}

		SolverResult res;
		try
		{
			res = sat.evaluate(cnf, null);
		} catch (IllegalSolverArgumentException e)
		{
			e.printStackTrace();
			return;
		}
		assertSame("doesn't detect cnf is unsat", SolverResultStatus.UNSATISFIABLE, res.getStatus());
	}

	@Test
	public void testSatInstance() {
		String cnfFile = "./tstcnf/sat.cnf";
		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}

		SolverResult res;
		try
		{
			res = sat.evaluate(cnf, null);
		} catch (IllegalSolverArgumentException e)
		{
			e.printStackTrace();
			return;
		}

		assertSame("doesn't detect cnf is sat", SolverResultStatus.SATISFIABLE, res.getStatus());
	}

	@Test
	public void testTimeOut() {
		String cnfFile = "./tstcnf/longue.cnf";
		SolverParameter param = sat.getRSatParameter();
		param.setTimeOut(BasicParameter.MIN_DELAY);
		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}

		SolverResult res;
		try
		{
			res = sat.evaluate(cnf, null);
		} catch (IllegalSolverArgumentException e)
		{
			// e.printStackTrace();
			return;
		}
		assertSame("doesn't detect timeout", SolverResultStatus.TIMEOUT_REACHED, res.getStatus());
	}

	@Test
	public void testCNFDoesntExist() {
		String cnfFile = "./tstcnf/.cnf";
		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			// e.printStackTrace();
			return;
		}

		SolverResult res;
		try
		{
			res = sat.evaluate(cnf, null);
		} catch (IllegalSolverArgumentException e)
		{
			// e.printStackTrace();
			return;
		}
		assertSame("doesn't detect cnf doesn't exist", SolverResultStatus.PROBLEM, res.getStatus());
	}

	@Test
	public void testStop() {
		String cnfFile = "./tstcnf/longue.cnf";
		// String out = "./cnf/newcnf.cnf";
		// param.setTimeOut(BasicParameter.MIN_DELAY);

		CNF cnf;
		try
		{
			cnf = new FileCNF(cnfFile);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}

		final Timer t = new Timer(500, null);
		t.addActionListener(new ActionListener() {
			@Override
			public void actionPerformed(ActionEvent e) {
				t.stop();
				sat.stop();
			}
		});

		SolverResult res;
		try
		{
			t.start();
			res = sat.evaluate(cnf, null);
		} catch (Exception e)
		{
			e.printStackTrace();
			return;
		}

		assertSame("problem with the use of stop function", SolverResultStatus.STOP, res.getStatus());
	}

}
